Inference at * 
Iof proof for Lemma can-apply-mu':


  A:Type, P:(A), d:(x:A. Dec(n:. ((P(x,n))))), x:A.
  (can-apply(mu'(P);x))  (n:. ((P(x,n)))) 

latex

 by (UnivCD THENA Auto) 
CollapseTHEN ((RepUR ``mu\' can-apply`` ( 0)) 
CollapseTHEN ((Subst' 
CTERMOF{p-mu-decider:ObjectId, 1:l, 1:l} ~ TERMOF{p-mu-decider:ObjectId, 1:l, i:l} ( 0)) 
THENL [
T(RW (SubC (ComputeToC []) ) 0) 
CollapseTHEN (Trivial) ; Id])) 

latex

C1: 

C1: 1. A : Type
C1: 2. P : A
C1: 3. d : x:A. Dec(n:. ((P(x,n))))
C1: 4. x : A
C1:   (isl((TERMOF{p-mu-decider:ObjectId, 1:l, i:l}(A,P,d,x)).1))  (n:. ((P(x,n))))
C.

Definitions	s ~ t, p-mu-decider, Dec(P), x:A. B(x), x:A  B(x), x:A. B(x), f(a), x:AB(x), , , t  T, Type, mu'(P), can-apply(f;x), b
Lemmas	decidable wf, assert wf, nat wf, bool wf